<!DOCTYPE HTML PUBLIC "-//W3C//DTD HTML 4.01 Transitional//EN" "http://www.w3.org/TR/html4/loose.dtd">
<!-- NewPage -->
<html lang="en">
<head>
<title>ScopeFrame</title>
<link rel="stylesheet" type="text/css" href="../../stylesheet.css" title="Style">
</head>
<body>
<script type="text/javascript"><!--
    if (location.href.indexOf('is-external=true') == -1) {
        parent.document.title="ScopeFrame";
    }
//-->
</script>
<noscript>
<div>JavaScript is disabled on your browser.</div>
</noscript>
<!-- ========= START OF TOP NAVBAR ======= -->
<div class="topNav"><a name="navbar_top">
<!--   -->
</a><a href="#skip-navbar_top" title="Skip navigation links"></a><a name="navbar_top_firstrow">
<!--   -->
</a>
<ul class="navList" title="Navigation">
<li><a href="../../overview-summary.html">Overview</a></li>
<li><a href="package-summary.html">Package</a></li>
<li class="navBarCell1Rev">Class</li>
<li><a href="package-tree.html">Tree</a></li>
<li><a href="../../deprecated-list.html">Deprecated</a></li>
<li><a href="../../index-all.html">Index</a></li>
<li><a href="../../help-doc.html">Help</a></li>
</ul>
</div>
<div class="subNav">
<ul class="navList">
<li><a href="../../mmj/lang/ScopeDef.html" title="class in mmj.lang"><span class="strong">Prev Class</span></a></li>
<li><a href="../../mmj/lang/Section.html" title="class in mmj.lang"><span class="strong">Next Class</span></a></li>
</ul>
<ul class="navList">
<li><a href="../../index.html?mmj/lang/ScopeFrame.html" target="_top">Frames</a></li>
<li><a href="ScopeFrame.html" target="_top">No Frames</a></li>
</ul>
<ul class="navList" id="allclasses_navbar_top">
<li><a href="../../allclasses-noframe.html">All Classes</a></li>
</ul>
<div>
<script type="text/javascript"><!--
  allClassesLink = document.getElementById("allclasses_navbar_top");
  if(window==top) {
    allClassesLink.style.display = "block";
  }
  else {
    allClassesLink.style.display = "none";
  }
  //-->
</script>
</div>
<div>
<ul class="subNavList">
<li>Summary:&nbsp;</li>
<li>Nested&nbsp;|&nbsp;</li>
<li><a href="#field_summary">Field</a>&nbsp;|&nbsp;</li>
<li><a href="#constructor_summary">Constr</a>&nbsp;|&nbsp;</li>
<li><a href="#method_summary">Method</a></li>
</ul>
<ul class="subNavList">
<li>Detail:&nbsp;</li>
<li><a href="#field_detail">Field</a>&nbsp;|&nbsp;</li>
<li><a href="#constructor_detail">Constr</a>&nbsp;|&nbsp;</li>
<li><a href="#method_detail">Method</a></li>
</ul>
</div>
<a name="skip-navbar_top">
<!--   -->
</a></div>
<!-- ========= END OF TOP NAVBAR ========= -->
<!-- ======== START OF CLASS DATA ======== -->
<div class="header">
<div class="subTitle">mmj.lang</div>
<h2 title="Class ScopeFrame" class="title">Class ScopeFrame</h2>
</div>
<div class="contentContainer">
<ul class="inheritance">
<li>java.lang.Object</li>
<li>
<ul class="inheritance">
<li>mmj.lang.ScopeFrame</li>
</ul>
</li>
</ul>
<div class="description">
<ul class="blockList">
<li class="blockList">
<hr>
<br>
<pre>public class <span class="strong">ScopeFrame</span>
extends java.lang.Object</pre>
<div class="block">A combined class representing <code>mandFrame</code>, the Mandatory "Frame" of an
 Assrt (assertion), as well as <code>optFrame</code>, the Optional "Frame" of a
 Theorem (OptFrame not present in other Assrt's).
 <p>
 Add <code>mandFrame</code> to <code>optFrame</code> and you have a Metamath
 "Extended Frame".</div>
<dl><dt><span class="strong">See Also:</span></dt><dd><a href="../../MetamathERNotes.html"> Nomenclature and
      Entity-Relationship Notes</a></dd></dl>
</li>
</ul>
</div>
<div class="summary">
<ul class="blockList">
<li class="blockList">
<!-- =========== FIELD SUMMARY =========== -->
<ul class="blockList">
<li class="blockList"><a name="field_summary">
<!--   -->
</a>
<h3>Field Summary</h3>
<table class="overviewSummary" border="0" cellpadding="3" cellspacing="0" summary="Field Summary table, listing fields, and an explanation">
<caption><span>Fields</span><span class="tabEnd">&nbsp;</span></caption>
<tr>
<th class="colFirst" scope="col">Modifier and Type</th>
<th class="colLast" scope="col">Field and Description</th>
</tr>
<tr class="altColor">
<td class="colFirst"><code><a href="../../mmj/lang/DjVars.html" title="class in mmj.lang">DjVars</a>[]</code></td>
<td class="colLast"><code><strong><a href="../../mmj/lang/ScopeFrame.html#djVarsArray">djVarsArray</a></strong></code>
<div class="block">These are the disjoint variable (pair)restrictions, if any, that apply to
 the Assrt and any of its proof steps.</div>
</td>
</tr>
<tr class="rowColor">
<td class="colFirst"><code><a href="../../mmj/lang/Hyp.html" title="class in mmj.lang">Hyp</a>[]</code></td>
<td class="colLast"><code><strong><a href="../../mmj/lang/ScopeFrame.html#hypArray">hypArray</a></strong></code>
<div class="block">These are the "mandatories" that are referenced in an assertion, in order
 of appearance in the database.</div>
</td>
</tr>
</table>
</li>
</ul>
<!-- ======== CONSTRUCTOR SUMMARY ======== -->
<ul class="blockList">
<li class="blockList"><a name="constructor_summary">
<!--   -->
</a>
<h3>Constructor Summary</h3>
<table class="overviewSummary" border="0" cellpadding="3" cellspacing="0" summary="Constructor Summary table, listing constructors, and an explanation">
<caption><span>Constructors</span><span class="tabEnd">&nbsp;</span></caption>
<tr>
<th class="colOne" scope="col">Constructor and Description</th>
</tr>
<tr class="altColor">
<td class="colOne"><code><strong><a href="../../mmj/lang/ScopeFrame.html#ScopeFrame()">ScopeFrame</a></strong>()</code>
<div class="block">Default Constructor.</div>
</td>
</tr>
<tr class="rowColor">
<td class="colOne"><code><strong><a href="../../mmj/lang/ScopeFrame.html#ScopeFrame(mmj.lang.ScopeDef, int)">ScopeFrame</a></strong>(<a href="../../mmj/lang/ScopeDef.html" title="class in mmj.lang">ScopeDef</a>&nbsp;scopeDef,
          int&nbsp;maxSeq)</code>
<div class="block">Builds a Frame using a ScopeDef and an array of Distinct Variables,
 limited by an input maximum sequence number.</div>
</td>
</tr>
<tr class="altColor">
<td class="colOne"><code><strong><a href="../../mmj/lang/ScopeFrame.html#ScopeFrame(mmj.lang.ScopeFrame, mmj.lang.ScopeFrame)">ScopeFrame</a></strong>(<a href="../../mmj/lang/ScopeFrame.html" title="class in mmj.lang">ScopeFrame</a>&nbsp;mandFrame,
          <a href="../../mmj/lang/ScopeFrame.html" title="class in mmj.lang">ScopeFrame</a>&nbsp;optFrame)</code>
<div class="block">Builds a composite ("combo") Frame using a MandFrame plus an OptFrame,
 augmented by additional $d specifications.</div>
</td>
</tr>
</table>
</li>
</ul>
<!-- ========== METHOD SUMMARY =========== -->
<ul class="blockList">
<li class="blockList"><a name="method_summary">
<!--   -->
</a>
<h3>Method Summary</h3>
<table class="overviewSummary" border="0" cellpadding="3" cellspacing="0" summary="Method Summary table, listing methods, and an explanation">
<caption><span>Methods</span><span class="tabEnd">&nbsp;</span></caption>
<tr>
<th class="colFirst" scope="col">Modifier and Type</th>
<th class="colLast" scope="col">Method and Description</th>
</tr>
<tr class="altColor">
<td class="colFirst"><code>void</code></td>
<td class="colLast"><code><strong><a href="../../mmj/lang/ScopeFrame.html#addDjVarGroups(mmj.lang.Var[][])">addDjVarGroups</a></strong>(<a href="../../mmj/lang/Var.html" title="class in mmj.lang">Var</a>[][]&nbsp;dvGroupArray)</code>
<div class="block">Accumulates an array of DvGroups into the djVarsArray.</div>
</td>
</tr>
<tr class="rowColor">
<td class="colFirst"><code>boolean</code></td>
<td class="colLast"><code><strong><a href="../../mmj/lang/ScopeFrame.html#areBothDjVarsInHypArray(mmj.lang.DjVars)">areBothDjVarsInHypArray</a></strong>(<a href="../../mmj/lang/DjVars.html" title="class in mmj.lang">DjVars</a>&nbsp;djVars)</code>
<div class="block">Checks to see whether or not both variables in a DjVars pair are
 referenced in the MandFrame's array of hypotheses.</div>
</td>
</tr>
<tr class="altColor">
<td class="colFirst"><code>static <a href="../../mmj/lang/DjVars.html" title="class in mmj.lang">DjVars</a>[]</code></td>
<td class="colLast"><code><strong><a href="../../mmj/lang/ScopeFrame.html#buildConsolidatedDvArray(mmj.pa.DistinctVariablesStmt[])">buildConsolidatedDvArray</a></strong>(<a href="../../mmj/pa/DistinctVariablesStmt.html" title="class in mmj.pa">DistinctVariablesStmt</a>[]&nbsp;distinctVariablesStmtArray)</code>
<div class="block">Converts an array of ProofWorksheet DistinctVariablesStmt objects into an
 array of DjVars objects.</div>
</td>
</tr>
<tr class="rowColor">
<td class="colFirst"><code>static java.util.List&lt;java.util.List&lt;<a href="../../mmj/lang/Var.html" title="class in mmj.lang">Var</a>&gt;&gt;</code></td>
<td class="colLast"><code><strong><a href="../../mmj/lang/ScopeFrame.html#consolidateDvGroups(mmj.lang.DjVars[])">consolidateDvGroups</a></strong>(<a href="../../mmj/lang/DjVars.html" title="class in mmj.lang">DjVars</a>[]&nbsp;dvArray)</code>
<div class="block">Attempts to do a good job consolidating pairs of disjoint variables into
 groups of three or more.</div>
</td>
</tr>
<tr class="altColor">
<td class="colFirst"><code>java.util.Map&lt;java.lang.String,<a href="../../mmj/lang/Var.html" title="class in mmj.lang">Var</a>&gt;</code></td>
<td class="colLast"><code><strong><a href="../../mmj/lang/ScopeFrame.html#getVarMap()">getVarMap</a></strong>()</code>
<div class="block">Builds and returns Var HashMap derived from the MandFrame hypArray.</div>
</td>
</tr>
<tr class="rowColor">
<td class="colFirst"><code>static boolean</code></td>
<td class="colLast"><code><strong><a href="../../mmj/lang/ScopeFrame.html#isVarPairInDjArray(mmj.lang.ScopeFrame, mmj.lang.Var, mmj.lang.Var)">isVarPairInDjArray</a></strong>(<a href="../../mmj/lang/ScopeFrame.html" title="class in mmj.lang">ScopeFrame</a>&nbsp;frame,
                  <a href="../../mmj/lang/Var.html" title="class in mmj.lang">Var</a>&nbsp;vLo,
                  <a href="../../mmj/lang/Var.html" title="class in mmj.lang">Var</a>&nbsp;vHi)</code>
<div class="block">Checks to see if a certain pair of variables is mentioned in a OptFrame's
 DjVars array.</div>
</td>
</tr>
<tr class="altColor">
<td class="colFirst"><code>static void</code></td>
<td class="colLast"><code><strong><a href="../../mmj/lang/ScopeFrame.html#loadDvGroupsIntoList(java.util.List, mmj.lang.Var[][])">loadDvGroupsIntoList</a></strong>(java.util.List&lt;<a href="../../mmj/lang/DjVars.html" title="class in mmj.lang">DjVars</a>&gt;&nbsp;arrayList,
                    <a href="../../mmj/lang/Var.html" title="class in mmj.lang">Var</a>[][]&nbsp;dvGroupArray)</code>
<div class="block">Accumulates new Distinct Variables into an List of DjVars pairs.</div>
</td>
</tr>
</table>
<ul class="blockList">
<li class="blockList"><a name="methods_inherited_from_class_java.lang.Object">
<!--   -->
</a>
<h3>Methods inherited from class&nbsp;java.lang.Object</h3>
<code>clone, equals, finalize, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait</code></li>
</ul>
</li>
</ul>
</li>
</ul>
</div>
<div class="details">
<ul class="blockList">
<li class="blockList">
<!-- ============ FIELD DETAIL =========== -->
<ul class="blockList">
<li class="blockList"><a name="field_detail">
<!--   -->
</a>
<h3>Field Detail</h3>
<a name="hypArray">
<!--   -->
</a>
<ul class="blockList">
<li class="blockList">
<h4>hypArray</h4>
<pre>public&nbsp;<a href="../../mmj/lang/Hyp.html" title="class in mmj.lang">Hyp</a>[] hypArray</pre>
<div class="block">These are the "mandatories" that are referenced in an assertion, in order
 of appearance in the database.
 <p>
 For a Theorem these include not only the variable hypotheses for
 variables referenced in the assertion's Formula, but the logical
 hypotheses in scope of the Theorem plus the variable hypotheses for
 variables referenced by *those* logical hypotheses.
 <p>
 For an <code>optFrame</code>, these include all Hyps in scope not present in
 the mandatory <code>hypArray</code>.</div>
</li>
</ul>
<a name="djVarsArray">
<!--   -->
</a>
<ul class="blockListLast">
<li class="blockList">
<h4>djVarsArray</h4>
<pre>public&nbsp;<a href="../../mmj/lang/DjVars.html" title="class in mmj.lang">DjVars</a>[] djVarsArray</pre>
<div class="block">These are the disjoint variable (pair)restrictions, if any, that apply to
 the Assrt and any of its proof steps.
 <p>
 For an <code>optFrame</code>, these include all DjVars (pairs) in scope not
 present in the mandatory <code>djVarsArray</code>.</div>
</li>
</ul>
</li>
</ul>
<!-- ========= CONSTRUCTOR DETAIL ======== -->
<ul class="blockList">
<li class="blockList"><a name="constructor_detail">
<!--   -->
</a>
<h3>Constructor Detail</h3>
<a name="ScopeFrame()">
<!--   -->
</a>
<ul class="blockList">
<li class="blockList">
<h4>ScopeFrame</h4>
<pre>public&nbsp;ScopeFrame()</pre>
<div class="block">Default Constructor.</div>
</li>
</ul>
<a name="ScopeFrame(mmj.lang.ScopeDef, int)">
<!--   -->
</a>
<ul class="blockList">
<li class="blockList">
<h4>ScopeFrame</h4>
<pre>public&nbsp;ScopeFrame(<a href="../../mmj/lang/ScopeDef.html" title="class in mmj.lang">ScopeDef</a>&nbsp;scopeDef,
          int&nbsp;maxSeq)</pre>
<div class="block">Builds a Frame using a ScopeDef and an array of Distinct Variables,
 limited by an input maximum sequence number. Convenience method for
 ProofAsst's use on a new theorem. ProofAsst allows new theorems, assuming
 that all variables and hypotheses used are in global scope, but it also
 provides a "LocAfter" statement specification, so maxSeq is input to
 restrict the contents of the new Frame. LogHyp's in the scopeDef are not
 loaded into the Frame -- not expected at global scope level, and global
 LogHyp's are not used in ProofAsst (haven't seen one yet, just saying).</div>
<dl><dt><span class="strong">Parameters:</span></dt><dd><code>scopeDef</code> - ScopeDef, intended to be global scope.</dd><dd><code>maxSeq</code> - MObj.seq must be < maxSeq</dd></dl>
</li>
</ul>
<a name="ScopeFrame(mmj.lang.ScopeFrame, mmj.lang.ScopeFrame)">
<!--   -->
</a>
<ul class="blockListLast">
<li class="blockList">
<h4>ScopeFrame</h4>
<pre>public&nbsp;ScopeFrame(<a href="../../mmj/lang/ScopeFrame.html" title="class in mmj.lang">ScopeFrame</a>&nbsp;mandFrame,
          <a href="../../mmj/lang/ScopeFrame.html" title="class in mmj.lang">ScopeFrame</a>&nbsp;optFrame)</pre>
<div class="block">Builds a composite ("combo") Frame using a MandFrame plus an OptFrame,
 augmented by additional $d specifications. Convenience method for
 ProofAsst's use with an existing theorem.</div>
<dl><dt><span class="strong">Parameters:</span></dt><dd><code>mandFrame</code> - a Theorem's MandFrame</dd><dd><code>optFrame</code> - a Theorem's OptFrame</dd></dl>
</li>
</ul>
</li>
</ul>
<!-- ============ METHOD DETAIL ========== -->
<ul class="blockList">
<li class="blockList"><a name="method_detail">
<!--   -->
</a>
<h3>Method Detail</h3>
<a name="isVarPairInDjArray(mmj.lang.ScopeFrame, mmj.lang.Var, mmj.lang.Var)">
<!--   -->
</a>
<ul class="blockList">
<li class="blockList">
<h4>isVarPairInDjArray</h4>
<pre>public static&nbsp;boolean&nbsp;isVarPairInDjArray(<a href="../../mmj/lang/ScopeFrame.html" title="class in mmj.lang">ScopeFrame</a>&nbsp;frame,
                         <a href="../../mmj/lang/Var.html" title="class in mmj.lang">Var</a>&nbsp;vLo,
                         <a href="../../mmj/lang/Var.html" title="class in mmj.lang">Var</a>&nbsp;vHi)</pre>
<div class="block">Checks to see if a certain pair of variables is mentioned in a OptFrame's
 DjVars array.
 <p>
 Note: vLo and vHi are automatically switched if vLo is not low.
 <p>
 Note: this function is the reason that DjVars vars are stored as "lo" and
 "hi". Low and High are irrelevant to the mathematics of this situation.
 But if the vars were stored randomly or arbitrarily, then twice as many
 comparisons would be needed here.</div>
<dl><dt><span class="strong">Parameters:</span></dt><dd><code>frame</code> - Scope Frame to inspect.</dd><dd><code>vLo</code> - the "low" variable in the pair.</dd><dd><code>vHi</code> - the "high" variable in the pair.</dd>
<dt><span class="strong">Returns:</span></dt><dd>true if param var pair in OptFrame DjVars array.</dd></dl>
</li>
</ul>
<a name="buildConsolidatedDvArray(mmj.pa.DistinctVariablesStmt[])">
<!--   -->
</a>
<ul class="blockList">
<li class="blockList">
<h4>buildConsolidatedDvArray</h4>
<pre>public static&nbsp;<a href="../../mmj/lang/DjVars.html" title="class in mmj.lang">DjVars</a>[]&nbsp;buildConsolidatedDvArray(<a href="../../mmj/pa/DistinctVariablesStmt.html" title="class in mmj.pa">DistinctVariablesStmt</a>[]&nbsp;distinctVariablesStmtArray)</pre>
<div class="block">Converts an array of ProofWorksheet DistinctVariablesStmt objects into an
 array of DjVars objects.</div>
<dl><dt><span class="strong">Parameters:</span></dt><dd><code>distinctVariablesStmtArray</code> - array of DistinctVariablesStmt object.</dd>
<dt><span class="strong">Returns:</span></dt><dd>array of DjVars objects.</dd></dl>
</li>
</ul>
<a name="loadDvGroupsIntoList(java.util.List, mmj.lang.Var[][])">
<!--   -->
</a>
<ul class="blockList">
<li class="blockList">
<h4>loadDvGroupsIntoList</h4>
<pre>public static&nbsp;void&nbsp;loadDvGroupsIntoList(java.util.List&lt;<a href="../../mmj/lang/DjVars.html" title="class in mmj.lang">DjVars</a>&gt;&nbsp;arrayList,
                        <a href="../../mmj/lang/Var.html" title="class in mmj.lang">Var</a>[][]&nbsp;dvGroupArray)</pre>
<div class="block">Accumulates new Distinct Variables into an List of DjVars pairs. The
 dvGroupArray is Var[][], array of Var arrays. Each Var array is of the
 form { x, y, z, ... } which generates DjVars for (x,y), (x,z), (y,z),
 etc. There is one Var array for each $d statement, in other words.
 Duplicate DjVars pairs are dropped without notice, as are pairs such as
 (x, x). Convenience method for ProofAsst's use with an existing theorem.</div>
<dl><dt><span class="strong">Parameters:</span></dt><dd><code>arrayList</code> - list of DjVars objects</dd><dd><code>dvGroupArray</code> - array of Var[] arrays.</dd></dl>
</li>
</ul>
<a name="consolidateDvGroups(mmj.lang.DjVars[])">
<!--   -->
</a>
<ul class="blockList">
<li class="blockList">
<h4>consolidateDvGroups</h4>
<pre>public static&nbsp;java.util.List&lt;java.util.List&lt;<a href="../../mmj/lang/Var.html" title="class in mmj.lang">Var</a>&gt;&gt;&nbsp;consolidateDvGroups(<a href="../../mmj/lang/DjVars.html" title="class in mmj.lang">DjVars</a>[]&nbsp;dvArray)</pre>
<div class="block">Attempts to do a good job consolidating pairs of disjoint variables into
 groups of three or more.
 <p>
 The input dvArray is assumed to be in ascending order according to
 DjVars.compareTo. We assume AND require that it be free from duplicates.
 Here is an example of dvArray -- sorted and with no duplicates:
 <p>
 
 <pre>
 [(a,b),(a,c),(a,d),(b,c),(b,d),(b,e),(c,d),(c,f)]
 </pre>
 
 The output List contains an ordered set of Lists of disjoint variables,
 sorted by the first Var character string in the list. Here is sample
 output for the example above:
 
 <pre>
 [ [a,b,c,d], [b,e], [c,f] ]
 </pre>
 
 The algorithm should be capable of consolidating $d's into </code>[
 [a,x,y,z], [b,x,y,z] ]</code>, as well as </code> [ [x,y,z,a], [x,y,z,b]
 ]</code>.
 <p>
 Note that within a DjVars object. varLo and varHi are loaded by Var.Id.
 Thus, for disjoint vars "a" and "b", varLo = a, and varHi = b. Also,
 varLo is never equal to varHi.</div>
<dl><dt><span class="strong">Parameters:</span></dt><dd><code>dvArray</code> - the input list of DjVars</dd>
<dt><span class="strong">Returns:</span></dt><dd>the list of distinct variable groups</dd></dl>
</li>
</ul>
<a name="areBothDjVarsInHypArray(mmj.lang.DjVars)">
<!--   -->
</a>
<ul class="blockList">
<li class="blockList">
<h4>areBothDjVarsInHypArray</h4>
<pre>public&nbsp;boolean&nbsp;areBothDjVarsInHypArray(<a href="../../mmj/lang/DjVars.html" title="class in mmj.lang">DjVars</a>&nbsp;djVars)</pre>
<div class="block">Checks to see whether or not both variables in a DjVars pair are
 referenced in the MandFrame's array of hypotheses.
 <p>
 Note: checks only the VarHyp's.</div>
<dl><dt><span class="strong">Parameters:</span></dt><dd><code>djVars</code> - -- DjVars object containing 2 variables to be checked
            against the variables referenced in the MandFrame hypArray.</dd>
<dt><span class="strong">Returns:</span></dt><dd>boolean -- true if both DjVars variables are present in hypArray,
         otherwise false.</dd></dl>
</li>
</ul>
<a name="addDjVarGroups(mmj.lang.Var[][])">
<!--   -->
</a>
<ul class="blockList">
<li class="blockList">
<h4>addDjVarGroups</h4>
<pre>public&nbsp;void&nbsp;addDjVarGroups(<a href="../../mmj/lang/Var.html" title="class in mmj.lang">Var</a>[][]&nbsp;dvGroupArray)</pre>
<div class="block">Accumulates an array of DvGroups into the djVarsArray.
 <p>
 FYI, a DvGroup is an array of at least 2 variables which are by
 definition supposed to be distinct from each other. So [ph th ch] is a
 DvGroup which could be obtained from a $d statement like "$d ph th ch $."</div>
<dl><dt><span class="strong">Parameters:</span></dt><dd><code>dvGroupArray</code> - array of array of disjoint variables.</dd></dl>
</li>
</ul>
<a name="getVarMap()">
<!--   -->
</a>
<ul class="blockListLast">
<li class="blockList">
<h4>getVarMap</h4>
<pre>public&nbsp;java.util.Map&lt;java.lang.String,<a href="../../mmj/lang/Var.html" title="class in mmj.lang">Var</a>&gt;&nbsp;getVarMap()</pre>
<div class="block">Builds and returns Var HashMap derived from the MandFrame hypArray. The
 returned map of Vars contains the vars returned from the MandFrame's
 VarHyps via getVar(), and does not seek out vars used in the formulas of
 LogHyps mentioned in the hypArray. Reason? The VarHyps for any LogHyps
 should *already* be in the MandFrame hypArray, by definition (of
 MandFrame). Convenience method for ProofAsst's use.</div>
<dl><dt><span class="strong">Returns:</span></dt><dd>Map of Vars for VarHyps in ScopeFrame.hypArray.</dd></dl>
</li>
</ul>
</li>
</ul>
</li>
</ul>
</div>
</div>
<!-- ========= END OF CLASS DATA ========= -->
<!-- ======= START OF BOTTOM NAVBAR ====== -->
<div class="bottomNav"><a name="navbar_bottom">
<!--   -->
</a><a href="#skip-navbar_bottom" title="Skip navigation links"></a><a name="navbar_bottom_firstrow">
<!--   -->
</a>
<ul class="navList" title="Navigation">
<li><a href="../../overview-summary.html">Overview</a></li>
<li><a href="package-summary.html">Package</a></li>
<li class="navBarCell1Rev">Class</li>
<li><a href="package-tree.html">Tree</a></li>
<li><a href="../../deprecated-list.html">Deprecated</a></li>
<li><a href="../../index-all.html">Index</a></li>
<li><a href="../../help-doc.html">Help</a></li>
</ul>
</div>
<div class="subNav">
<ul class="navList">
<li><a href="../../mmj/lang/ScopeDef.html" title="class in mmj.lang"><span class="strong">Prev Class</span></a></li>
<li><a href="../../mmj/lang/Section.html" title="class in mmj.lang"><span class="strong">Next Class</span></a></li>
</ul>
<ul class="navList">
<li><a href="../../index.html?mmj/lang/ScopeFrame.html" target="_top">Frames</a></li>
<li><a href="ScopeFrame.html" target="_top">No Frames</a></li>
</ul>
<ul class="navList" id="allclasses_navbar_bottom">
<li><a href="../../allclasses-noframe.html">All Classes</a></li>
</ul>
<div>
<script type="text/javascript"><!--
  allClassesLink = document.getElementById("allclasses_navbar_bottom");
  if(window==top) {
    allClassesLink.style.display = "block";
  }
  else {
    allClassesLink.style.display = "none";
  }
  //-->
</script>
</div>
<div>
<ul class="subNavList">
<li>Summary:&nbsp;</li>
<li>Nested&nbsp;|&nbsp;</li>
<li><a href="#field_summary">Field</a>&nbsp;|&nbsp;</li>
<li><a href="#constructor_summary">Constr</a>&nbsp;|&nbsp;</li>
<li><a href="#method_summary">Method</a></li>
</ul>
<ul class="subNavList">
<li>Detail:&nbsp;</li>
<li><a href="#field_detail">Field</a>&nbsp;|&nbsp;</li>
<li><a href="#constructor_detail">Constr</a>&nbsp;|&nbsp;</li>
<li><a href="#method_detail">Method</a></li>
</ul>
</div>
<a name="skip-navbar_bottom">
<!--   -->
</a></div>
<!-- ======== END OF BOTTOM NAVBAR ======= -->
</body>
</html>
